Termination Proof Script
Consider the TRS R consisting of the rewrite rules
|
| 1: |
|
ge(x,0) |
→ true |
| 2: |
|
ge(0,s(x)) |
→ false |
| 3: |
|
ge(s(x),s(y)) |
→ ge(x,y) |
| 4: |
|
minus(x,0) |
→ x |
| 5: |
|
minus(s(x),s(y)) |
→ minus(x,y) |
| 6: |
|
div(x,y) |
→ ify(ge(y,s(0)),x,y) |
| 7: |
|
ify(false,x,y) |
→ divByZeroError |
| 8: |
|
ify(true,x,y) |
→ if(ge(x,y),x,y) |
| 9: |
|
if(false,x,y) |
→ 0 |
| 10: |
|
if(true,x,y) |
→ s(div(minus(x,y),y)) |
|
There are 8 dependency pairs:
|
| 11: |
|
GE(s(x),s(y)) |
→ GE(x,y) |
| 12: |
|
MINUS(s(x),s(y)) |
→ MINUS(x,y) |
| 13: |
|
DIV(x,y) |
→ IFY(ge(y,s(0)),x,y) |
| 14: |
|
DIV(x,y) |
→ GE(y,s(0)) |
| 15: |
|
IFY(true,x,y) |
→ IF(ge(x,y),x,y) |
| 16: |
|
IFY(true,x,y) |
→ GE(x,y) |
| 17: |
|
IF(true,x,y) |
→ DIV(minus(x,y),y) |
| 18: |
|
IF(true,x,y) |
→ MINUS(x,y) |
|
The approximated dependency graph contains 3 SCCs:
{11},
{12}
and {13,15,17}.
-
Consider the SCC {11}.
There are no usable rules.
By taking the AF π with
π(GE) = 1 together with
the lexicographic path order with
empty precedence,
rule 11
is strictly decreasing.
-
Consider the SCC {12}.
There are no usable rules.
By taking the AF π with
π(MINUS) = 1 together with
the lexicographic path order with
empty precedence,
rule 12
is strictly decreasing.
-
Consider the SCC {13,15,17}.
The usable rules are {1-5}.
The constraints could not be solved.
Tyrolean Termination Tool (0.45 seconds)
--- May 4, 2006